Verification of Local-First Software

Seminar, Project

Verification of local-first software (and distributed software in general) is challenging because it is insufficient to only reason about the local behaviour of a program. Instead, we have to account for operations that can happen concurrently on multiple devices. Existing approaches employ advanced type systems, deductive program verification, model checking or combinations thereof.

In this topic, you will explore the current state of verification approaches in the local first-domain (seminar) or implement your own/extend existing ones (project).